(x unchanged-for t @ e)
== (x changed before e)
==  qle((es-time(es; (last change to x before e)) + t); es-time(es; e)) 

latex

---

clarification:

unchanged-for{i:l}
unchanged-for(T; eq; es; x; t; e)
== (changed{i:l}
== (changed(T; eq; es; x; e))
==  qle((es-time(es; last-change{i:l}(T; eq; es; x; e)) + t); es-time(es; e)) 

latex

Definitions	P  Q, b, x changed before e, qle(r; s), r + s, (last change to x before e), es-time(es; e)
FDL editor aliases	unchanged-for